<html>
<head><meta charset="utf-8"><title>hacspec · wg-secure-code · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/index.html">wg-secure-code</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/hacspec.html">hacspec</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="184879338"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/hacspec/near/184879338" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Tony Arcieri <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/hacspec.html#184879338">(Jan 06 2020 at 04:30)</a>:</h4>
<p>This is pretty interesting: <a href="https://twitter.com/bascule/status/1213937672676356096" target="_blank" title="https://twitter.com/bascule/status/1213937672676356096">https://twitter.com/bascule/status/1213937672676356096</a></p>
<div class="inline-preview-twitter"><div class="twitter-tweet"><a href="https://twitter.com/bascule/status/1213937672676356096" target="_blank"><img class="twitter-avatar" src="https://pbs.twimg.com/profile_images/450061818606522368/pjDTHFB9_normal.jpeg"></a><p>hacspec-rust: reference specifications of various cryptographic algorithms written in a subset of <a href="https://twitter.com/rustlang" target="_blank" title="https://twitter.com/rustlang">@rustlang</a>:
<a href="https://t.co/UwgaGgr8qV" target="_blank" title="https://t.co/UwgaGgr8qV">https://github.com/hacspec/hacspecs-rust/tree/master/src</a></p><span>- Tony “Abolish ICE” Arcieri 🦀 (@bascule)</span></div></div>



<a name="184971257"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/hacspec/near/184971257" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Shnatsel <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/hacspec.html#184971257">(Jan 07 2020 at 00:20)</a>:</h4>
<p>Oooh, that's pretty cool</p>



<a name="185594972"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/hacspec/near/185594972" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> franziskus <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/hacspec.html#185594972">(Jan 14 2020 at 13:25)</a>:</h4>
<p>We're still in pretty early stages here. But I hope we have something to show in a couple months, i.e. a proper formalisation and a comprehensive hacspec library. But let me know if you're interested in helping <span aria-label="slight smile" class="emoji emoji-1f642" role="img" title="slight smile">:slight_smile:</span></p>



<a name="185595100"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/hacspec/near/185595100" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alex Gaynor <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/hacspec.html#185595100">(Jan 14 2020 at 13:27)</a>:</h4>
<p>Is this the next step of HACL*?</p>



<a name="185595251"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/hacspec/near/185595251" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> franziskus <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/hacspec.html#185595251">(Jan 14 2020 at 13:29)</a>:</h4>
<p>We want to be able to generate the specs in HACL* from this, yes. So it's not replacing HACL* but should make it easier to write the specs that are used as starting point for the correctness proofs</p>



<a name="185595331"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/146229-wg-secure-code/topic/hacspec/near/185595331" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> franziskus <a href="https://rust-lang.github.io/zulip_archive/stream/146229-wg-secure-code/topic/hacspec.html#185595331">(Jan 14 2020 at 13:30)</a>:</h4>
<p>ideally we want more than only F* as target though. cryptol and coq for example would be nice (in case someone is interested in writing those compilers <span aria-label="smiley" class="emoji emoji-1f603" role="img" title="smiley">:smiley:</span> )</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>